@$i$: only $L$ affects $x$ : $t$($j$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$)$\rightarrow$ only members of $L$ affect $x$ :$t$ else fi